YES 1.891 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule List
  ((isSuffixOf :: (Eq b, Eq a) => [(b,a)]  ->  [(b,a)]  ->  Bool) :: (Eq a, Eq b) => [(b,a)]  ->  [(b,a)]  ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] _ True
isPrefixOf [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule List
  ((isSuffixOf :: (Eq b, Eq a) => [(b,a)]  ->  [(b,a)]  ->  Bool) :: (Eq b, Eq a) => [(b,a)]  ->  [(b,a)]  ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule List
  (isSuffixOf :: (Eq b, Eq a) => [(a,b)]  ->  [(a,b)]  ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xy6200), Succ(xy3501000)) → new_primPlusNat(xy6200, xy3501000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xy32100), Succ(xy350100)) → new_primMulNat(xy32100, Succ(xy350100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xy3200), Succ(xy35000)) → new_primEqNat(xy3200, xy35000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, app(app(ty_@2, fh), ga), ea) → new_esEs1(xy321, xy3501, fh, ga)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), app(app(app(ty_@3, hh), baa), bab), hg) → new_esEs0(xy320, xy3500, hh, baa, bab)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), bag, app(ty_Maybe, bbh)) → new_esEs3(xy321, xy3501, bbh)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), app(app(ty_Either, he), hf), hg) → new_esEs(xy320, xy3500, he, hf)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), app(ty_Maybe, eh), dh, ea) → new_esEs3(xy320, xy3500, eh)
new_esEs2(:(xy320, xy321), :(xy3500, xy3501), app(ty_Maybe, bda)) → new_esEs3(xy320, xy3500, bda)
new_esEs3(Just(xy320), Just(xy3500), app(app(ty_@2, bdh), bea)) → new_esEs1(xy320, xy3500, bdh, bea)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), app(app(ty_Either, df), dg), dh, ea) → new_esEs(xy320, xy3500, df, dg)
new_esEs(Left(xy320), Left(xy3500), app(app(ty_@2, bg), bh), bc) → new_esEs1(xy320, xy3500, bg, bh)
new_esEs3(Just(xy320), Just(xy3500), app(ty_[], beb)) → new_esEs2(xy320, xy3500, beb)
new_esEs(Right(xy320), Right(xy3500), cc, app(ty_Maybe, de)) → new_esEs3(xy320, xy3500, de)
new_esEs2(:(xy320, xy321), :(xy3500, xy3501), app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs0(xy320, xy3500, bcc, bcd, bce)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), app(ty_[], eg), dh, ea) → new_esEs2(xy320, xy3500, eg)
new_esEs(Right(xy320), Right(xy3500), cc, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xy320, xy3500, cf, cg, da)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, dh, app(app(ty_Either, gd), ge)) → new_esEs(xy322, xy3502, gd, ge)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), app(ty_Maybe, baf), hg) → new_esEs3(xy320, xy3500, baf)
new_esEs(Left(xy320), Left(xy3500), app(ty_[], ca), bc) → new_esEs2(xy320, xy3500, ca)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), app(ty_[], bae), hg) → new_esEs2(xy320, xy3500, bae)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, app(app(app(ty_@3, fd), ff), fg), ea) → new_esEs0(xy321, xy3501, fd, ff, fg)
new_esEs(Left(xy320), Left(xy3500), app(app(app(ty_@3, bd), be), bf), bc) → new_esEs0(xy320, xy3500, bd, be, bf)
new_esEs3(Just(xy320), Just(xy3500), app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs0(xy320, xy3500, bde, bdf, bdg)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, app(ty_Maybe, gc), ea) → new_esEs3(xy321, xy3501, gc)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), bag, app(ty_[], bbg)) → new_esEs2(xy321, xy3501, bbg)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, dh, app(ty_Maybe, hd)) → new_esEs3(xy322, xy3502, hd)
new_esEs2(:(xy320, xy321), :(xy3500, xy3501), app(app(ty_Either, bca), bcb)) → new_esEs(xy320, xy3500, bca, bcb)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), bag, app(app(ty_@2, bbe), bbf)) → new_esEs1(xy321, xy3501, bbe, bbf)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, dh, app(app(ty_@2, ha), hb)) → new_esEs1(xy322, xy3502, ha, hb)
new_esEs(Right(xy320), Right(xy3500), cc, app(ty_[], dd)) → new_esEs2(xy320, xy3500, dd)
new_esEs(Right(xy320), Right(xy3500), cc, app(app(ty_Either, cd), ce)) → new_esEs(xy320, xy3500, cd, ce)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, app(ty_[], gb), ea) → new_esEs2(xy321, xy3501, gb)
new_esEs2(:(xy320, xy321), :(xy3500, xy3501), app(app(ty_@2, bcf), bcg)) → new_esEs1(xy320, xy3500, bcf, bcg)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, dh, app(app(app(ty_@3, gf), gg), gh)) → new_esEs0(xy322, xy3502, gf, gg, gh)
new_esEs2(:(xy320, xy321), :(xy3500, xy3501), bdb) → new_esEs2(xy321, xy3501, bdb)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), app(app(ty_@2, bac), bad), hg) → new_esEs1(xy320, xy3500, bac, bad)
new_esEs3(Just(xy320), Just(xy3500), app(ty_Maybe, bec)) → new_esEs3(xy320, xy3500, bec)
new_esEs(Left(xy320), Left(xy3500), app(ty_Maybe, cb), bc) → new_esEs3(xy320, xy3500, cb)
new_esEs3(Just(xy320), Just(xy3500), app(app(ty_Either, bdc), bdd)) → new_esEs(xy320, xy3500, bdc, bdd)
new_esEs(Right(xy320), Right(xy3500), cc, app(app(ty_@2, db), dc)) → new_esEs1(xy320, xy3500, db, dc)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, dh, app(ty_[], hc)) → new_esEs2(xy322, xy3502, hc)
new_esEs2(:(xy320, xy321), :(xy3500, xy3501), app(ty_[], bch)) → new_esEs2(xy320, xy3500, bch)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), app(app(ty_@2, ee), ef), dh, ea) → new_esEs1(xy320, xy3500, ee, ef)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), fa, app(app(ty_Either, fb), fc), ea) → new_esEs(xy321, xy3501, fb, fc)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), bag, app(app(ty_Either, bah), bba)) → new_esEs(xy321, xy3501, bah, bba)
new_esEs(Left(xy320), Left(xy3500), app(app(ty_Either, ba), bb), bc) → new_esEs(xy320, xy3500, ba, bb)
new_esEs0(@3(xy320, xy321, xy322), @3(xy3500, xy3501, xy3502), app(app(app(ty_@3, eb), ec), ed), dh, ea) → new_esEs0(xy320, xy3500, eb, ec, ed)
new_esEs1(@2(xy320, xy321), @2(xy3500, xy3501), bag, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs0(xy321, xy3501, bbb, bbc, bbd)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf(:(xy310, xy311), :(xy3510, xy3511), ba) → new_isPrefixOf(xy311, xy3511, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf0(xy32, xy31, xy35, :(xy3410, xy3411), ba) → new_isPrefixOf0(xy32, xy31, new_flip(xy35, xy3410, ba), xy3411, ba)

The TRS R consists of the following rules:

new_flip(xy31, xy32, ba) → :(xy32, xy31)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf1(xy31, xy32, :(xy330, xy331), xy34, ba) → new_isPrefixOf1(new_flip(xy31, xy32, ba), xy330, xy331, xy34, ba)

The TRS R consists of the following rules:

new_flip(xy31, xy32, ba) → :(xy32, xy31)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: